\relax 
\citation{Mossakowski-Maeder-Luttich:2007,Franssen-Brand:2009,Hemer-Long-Strooper:2005,uitp-web-page,Aspinall-Luth:2007}
\citation{CDELMMQ:2002,CDELMMT:2007-book}
\citation{clavel99,CDHLMO:2007}
\citation{CDHLMO:2007}
\citation{Duran-Meseguer:2007-scp,CDELMMT:2007-book}
\citation{Duran-Olveczky:2008-wrla}
\@writefile{toc}{\contentsline {title}{Towards a Maude Formal Environment}{1}}
\@writefile{toc}{\authcount {3}}
\@writefile{toc}{\contentsline {author}{Francisco Dur\'an\unskip {} \and Camilo Rocha\unskip {} \and Jos\'e M. \'Alvarez\unskip {}}{1}}
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}}
\newlabel{sec.intro}{{1}{1}}
\citation{Duran-Lucas-Meseguer:2008-ijcar}
\citation{Duran-Meseguer:2010-wrla-crc,Duran-Meseguer:2011}
\citation{Duran-Meseguer:2010-wrla-chc,Duran-Meseguer:2011}
\citation{Hendrix-Clavel-Meseguer:05,Hendrix-Meseguer-Ohsaki:2006}
\citation{Clavel-Palomino-Riesco:2006,Hendrix:2008}
\citation{Hendrix:2008}
\citation{CDELMMT:2007-book}
\@writefile{toc}{\contentsline {paragraph}{\bf  Outline of the paper.}{2}}
\@writefile{toc}{\contentsline {section}{\numberline {2}Object-Based Programming and User Interfaces in Maude}{2}}
\newlabel{sec.prelim}{{2}{2}}
\citation{CDELMMT:2007-book}
\@writefile{toc}{\contentsline {paragraph}{\bf  Object-based programming.}{3}}
\@writefile{toc}{\contentsline {paragraph}{\bf  User interfaces.}{4}}
\@writefile{toc}{\contentsline {paragraph}{\bf  Full Maude.}{4}}
\@writefile{toc}{\contentsline {section}{\numberline {3}The Design of MFE}{5}}
\newlabel{sec.design}{{3}{5}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}Proof Objects}{5}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Tool Objects}{6}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}The Controller Object}{7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}User Interaction and Tool Interoperability}{8}}
\citation{Duran-Lucas-Meseguer:2009-prole,Duran-Lucas-Meseguer:2009-frocos}
\@writefile{toc}{\contentsline {section}{\numberline {4}Tools in MFE}{9}}
\newlabel{sec.tools}{{4}{9}}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Tool-dependency graph in MFE.}}{9}}
\newlabel{fig.tool-dep}{{1}{9}}
\citation{Lucas:2004}
\citation{Giesl-Schneider-Kamp-Thiemann:2006}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}The Maude Termination Tool}{10}}
\newlabel{sec.mtt}{{4.1}{10}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}The Church-Rosser Checker}{10}}
\newlabel{sec.crc}{{4.2}{10}}
\citation{Rocha-Meseguer:2010,Hendrix:2008}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3}The Coherence Checker}{11}}
\newlabel{sec.chc}{{4.3}{11}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.4}The Sufficient Completeness Checker}{11}}
\newlabel{sec.scc}{{4.4}{11}}
\citation{Rocha-Meseguer:2010,Hendrix:2008}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.5}The Maude Inductive Theorem Prover}{12}}
\newlabel{sec.itp}{{4.5}{12}}
\@writefile{toc}{\contentsline {section}{\numberline {5}Extensibility by Example: the Integration of SCC}{12}}
\newlabel{sec.extend}{{5}{12}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}SCC Proof Objects}{12}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}The SCC Tool Object}{13}}
\@writefile{toc}{\contentsline {paragraph}{\bf  Dependencies.}{15}}
\citation{CDELMMT:2007-book}
\citation{CDELMMT:2007-book}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Making SCC Operational in MFE}{16}}
\@writefile{toc}{\contentsline {section}{\numberline {6}Using MFE}{16}}
\newlabel{sec.example}{{6}{16}}
\citation{CDELMMT:2007-book}
\citation{CDELMMT:2007-book}
\@writefile{toc}{\contentsline {section}{\numberline {7}Conclusion}{21}}
\newlabel{sec.concl}{{7}{21}}
\bibstyle{splncs03}
\bibcite{uitp-web-page}{1}
\bibcite{Aspinall-Luth:2007}{2}
\bibcite{CDELMMQ:2002}{3}
\bibcite{CDELMMT:2007-book}{4}
\bibcite{clavel99}{5}
\bibcite{CDHLMO:2007}{6}
\bibcite{Clavel-Palomino-Riesco:2006}{7}
\bibcite{Duran-Lucas-Meseguer:2008-ijcar}{8}
\bibcite{Duran-Lucas-Meseguer:2009-prole}{9}
\bibcite{Duran-Lucas-Meseguer:2009-frocos}{10}
\bibcite{Duran-Meseguer:2007-scp}{11}
\bibcite{Duran-Meseguer:2010-wrla-chc}{12}
\bibcite{Duran-Meseguer:2010-wrla-crc}{13}
\@writefile{toc}{\contentsline {paragraph}{\bf  Acknowledgements.}{22}}
\bibcite{Duran-Meseguer:2011}{14}
\bibcite{Duran-Olveczky:2008-wrla}{15}
\bibcite{Franssen-Brand:2009}{16}
\bibcite{Giesl-Schneider-Kamp-Thiemann:2006}{17}
\bibcite{Hemer-Long-Strooper:2005}{18}
\bibcite{Hendrix:2008}{19}
\bibcite{Hendrix-Clavel-Meseguer:05}{20}
\bibcite{Hendrix-Meseguer-Ohsaki:2006}{21}
\bibcite{Lucas:2004}{22}
\bibcite{Mossakowski-Maeder-Luttich:2007}{23}
\bibcite{Rocha-Meseguer:2010}{24}
